(* $Id: simplify.ml 95 2007-10-17 19:56:09Z yann.regisgianas $ *)

(* Pangolin, a functional programming language for correct programs.
   Copyright (C) 2007, Yann Régis-Gianas, François Pottier.
   Contact: yann.regisgianas@gmail.com

   This program is free software: you can redistribute it and/or modify
   it under the terms of the GNU General Public License as published by
   the Free Software Foundation, either version 3 of the License, or
   any later version.

   This program is distributed in the hope that it will be useful,
   but WITHOUT ANY WARRANTY; without even the implied warranty of
   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
   GNU General Public License for more details.

   You should have received a copy of the GNU General Public License
   along with this program.  If not, see <http://www.gnu.org/licenses/>. *)

open PFOLSyntax
open PFOLSyntax.Raw
open SimplifyPrinter

let timeout = ref 5
let remove = ref false

let simplify_command () = 
  (Printf.sprintf "timeout %d %s" !timeout Configuration.simplify)

module C = Misc.Cache 
  (struct type t = string * string
	  let hash (_, g) = Hashtbl.hash g 
	  let equal (f1, g1) (f2, g2) =
	    String.compare g1 g2 = 0 && String.compare f1 f2 = 0
   end)
  (struct type t = bool * string end)

let cache_fun = ref (fun f x -> f x)
let close_fun = ref ignore

let init_cache filename = 
  let (cache, close) = C.cache_in_file filename in
    cache_fun := cache;
    close_fun := close

let save_cache () = 
  !close_fun ()

let if_not_removed remove filename = 
  if remove then "" else "(filename: "^ filename ^")"

let launch_simplify command matching_output q =
  Misc.tmp_filename_from_string ~remove:!remove ".sx"
    q
    (fun filename -> 
       match 
	 Sys.command 
	   (Printf.sprintf 
	      "%s %s | grep \"%s\" 1> /dev/null 2> /dev/null" 
	      (command ())
	      filename
	      matching_output) 
       with
	 | 0 -> (true, if_not_removed !remove filename)
	 | _ -> (false, if_not_removed !remove filename))


let prove (q, _) = 
  launch_simplify simplify_command "Valid" q 

let tries = ref 0
let success = ref 0

let prove q = 
  incr tries;
  let (ret, filename) = !cache_fun prove (print q) in
    if ret then incr success;
    (ret, filename)

let inconsistent_assumptions q = 
  prove q

let print_stats () =
  Printf.printf "Simplify made %d proofs over %d proof obligations.\n"
    !success !tries
